Skip to content

Instantly share code, notes, and snippets.

@cr1901

cr1901/how_i_got_started.md Secret

Created August 11, 2017 01:30
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save cr1901/a445ef31281e67a0cf286e149deaac41 to your computer and use it in GitHub Desktop.
Save cr1901/a445ef31281e67a0cf286e149deaac41 to your computer and use it in GitHub Desktop.
Download ZIP
Incomplete notes for getting started with temporal induction.
Raw
how_i_got_started.md

Prerequisites

  • Know Verilog and One Other Programming Language
  • Watch Lectures 0-7 of Hehner's A Practical Theory of Programming Course
    • Sit on it for a few days to a week (you'll prob be confused)
    • Up to and including Quantifiers should be fine
    • You may wish to do some the textbook problems
  • Familiarity w/ Lisp syntax
  • Read slides #25 to the end of this slide deck
  • You may want to take a quick look at the z3 Guide.
  • yosys, yosys-smtbmc, and z3 installed

What you'll prob notice after prereqs

  • You will begin to recognize the terminology used in Wikipedia articles on logic ("predicate", "statements assumed to be true", "theory")
    • Term "theory" is thrown around a lot
  • APToP looks kinda like a logic one would use for SMT.
  • What are BitVectors/Uninterpreted Functions/Arrays?

What next? This describes what I did to learn more, including missteps.

Notes on SMT

SAT vs SMT

  • SAT is "given a set of boolean expressions and variables, can I make all the expressions true by using specific values for all the variables?"
    • For example, (x AND y) OR z is a boolean expression consisting of AND and OR operators.
  • SMT is SAT on steroids. We have extra entities besides boolean variables/expressions we can manipulate, and associated "rules" for manipulation called theories. The expressions that need to be true can also use these new entities.

What Do I Mean By Theories?

When I discuss theories, I mean the mathematical definition of theory. Personally, for our purposes I think it's just easier to informally see a theory described, at which point you can extrapolate for how to define a theory for another object. So let me just give an example of a theory (Boolean Logic). Note that this is reiterating parts of Hehner's first lecture using English instead of symbols. The purpose of watching Lectures 0-7 is to get a feel for how to define theories, manipulate expressions, and recognize statements about entities that remain logically true no matter how you manipulate these entities.

Abbreviated/Informal Boolean Theory

  • Boolean variables can take on one of two values- true or false.
  • Boolean logic has its own way to manipulate- change/create- boolean types (operators):
    • AND, OR, NOT, NAND, NOR, XOR, XNOR are prob familiar.
    • There are extra manipulations you can define:
      • x EQ y: true if x equals y, otherwise false
      • x IMPLIES y: If x is true, y must be true for the whole expression to be true. If x is false, x IMPLIES y is true; y's value is irrelevant.
      • x IMPLIED_BY y: If y is true, x must be true for the whole expression to be true. If y is false, x IMPLIED_BY y is true; x's value is irrelevant.
      • IF x THEN y ELSE z: Use the value of y if x is true, otherwise use the value of z (x, y, and z are booleans or an expression that returns a boolean)
  • We can chain operators together to create expressions.

Other entities, such as Lists, have their own sets of operators and "rules" for manipulation that make a theory. Not all operators are compatible w/ each other (for example, we can't OR a bool and a list), but we can define operators/"rules" that return other entities. For instance, the answer to the question "Are two lists are equal to each other?" is either yes or no, or true or false- a bool! List equality could thus be defined as taking two Lists and returning a bool.

What's The Goal?

  1. We create some statements that define new rules for how our variables can be manipulated based on the existing theories.
  2. We create a number of statements that we assume are true, and want to know whether these statements are in fact true for some set of input variables in #1, when we allow manipulations of variables based on the theories and statements in #1. We call these assertions.
  3. The SMT solver runs an algorithm to figure out whether, by setting all input variables to values, we can make all statements in #2 true.
  • If we find a set of inputs which make all of our assertions true, the SMT solver returns SAT. Otherwise the solver returns UNSAT.

How Do I Create Variables?

  • Some functions are left for the SMT solver to "fill in". All we do is specify the input and output. For instance, I can create L1 MysteryOp L2 function/operator, which takes two lists and returns a bool. It's up to the SMT solver to determine what MysteryOp actually does based on List Theory, but it better take in two Lists and output a bool!
    • These are known as Uninterpreted Functions. Like Lists, integers, and booleans, they also have a theory associated with them.
  • Some (many?) variables in expressions will also have some of their values left unspecified.
  • Both Uninterpreted Functions and variables whose values are unspecified become input variables to the entire system of statements. Outputs of and intermediate variables within the system of statements become subject to assertions- the statements we wish to know whether or not we can make true for at least one set of input variables.

Example Of Using An SMT Solver

SMTv2 is a file format that defines statements that SMT solvers understand and can be used to create scripts for systems that you want to prove meet/do not meet certain conditions.

A contrived example using the scripting capabilities of the SMTv2 interchange format is shown on the z3 guide, which I reproduce here:

(declare-const a Int)
(declare-fun f (Int Bool) Int)
(assert (> a 10))
(assert (< (f a true) 100))
(check-sat)
(get-model)

Let's walk through each line:

  1. (declare-const a Int): This declares a constant a of type Int, for integer. Like bools and Lists, integers have their own separate theory! a can now be used later for any purpose we feel like; we know it's an integer, but we don't know which integer (could be 0, 1, 999).
  2. (declare-fun f (Int Bool) Int): This creates an Uninterpreted Function. f is a function take takes in an integer and bool, and returns an int. I have no idea what expressions make up this function right now, but I know that the expressions that make up the function will leave an integer and bool "free" for input and return an integer as output.
  • (declare-const a Int) is shorthand for (declare-fun a () Int). This makes sense to me, as if you're not inputting anything, but getting an output, what's the point of doing anything except just returning the output immediately?
  1. (assert (> a 10)): Our first assertion. We need our constant a to be greater than 10 for this statement to be true.
  2. (assert (< (f a true) 100)): Our second assertion. We need our function f, given the input a (same a as defined in #1) and a true boolean input value, to return an integer less than 100 for this statement to be true.
  3. (check-sat): Find an example, if one exists, of a and f that makes the assertions defined in #3 and #4 true.
  4. (get-model): If SAT, z3 will tell me "how did z3 define a and f to make the assertions true"?

If we run the code snippet by trying z3 online, we find that the entire system of statements is SAT. The SMT solver for me chose the following inputs/model:

sat
(model 
  (define-fun a () Int 11)
  (define-fun f ((x!1 Int) (x!2 Bool)) Int 
    (ite (and (= x!1 11) (= x!2 true)) 0 0))
)

define-fun actually specifies how a function should behave by defining expressions while leaving the inputs x!1 and x!2 as free variables (i.e. "any value valid for an integer and bool"). ite is "if then else", analogous to "if-else statements" in most programming languages.

An Example Verilog Program

Instead of using Bunches, Sets, Strings, and Lists, as described in APToP, we use BitVectors, Arrays, and Uninterpreted Functions for z3 Uninterpreted Function, BitVector and Array Theory is described in the z3 Guide,
so read that and we can go on to the next section!

Blatantly stolen from Clifford Wolf's examples:

module hello(input clk, input rst, output [3:0] cnt);
  reg [3:0] cnt = 0;

  always @(posedge clk) begin
    if (rst)
      cnt <= 0;
    else
      cnt <= cnt + 1;
  end

`ifdef FORMAL
  assume property (cnt != 10);
  assert property (cnt != 15);
`endif
endmodule

It's a 4-bit counter! yosys is capable of converting Verilog code into functions and logic that an SMT solver can understand. The verilog code defines the rules for how our inputs can be manipulated to produce outputs.

`yosys-smtb

So Why yosys-smtbmc Then?

The SMTv2 output from yosys can be input into a SMT solver just fine. As-is, the SMTv2 output produced by yosys isn't enough to actually do the types of proofs we want. All the boiler-plate is there however, including transitioning from state n to state n + 1.

For Bounded Model Check (BMC) SAT is actually the fail condition, and provides a counterexample showing a set of inputs over time that cause the conditions to fail

Gotchas

  • Forgetting clock2dff pass in a multi-clock design

  • my_hello1

  • Sometimes you will see expressions like: (or (|hello#3| state) (not true)), where the or or and operator is unnecessary. This is a side-effect of how yosys generates SMT2 files in the backend. In other contexts, (not true) would be an expression with variables.

[z3_guide] : http://rise4fun.com/z3/tutorialcontent/guide

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment