This commit is contained in:
Julin S 2023-04-26 22:34:49 +05:30
parent c800042ddb
commit 19b46bf36d
17 changed files with 515 additions and 0 deletions

18
nusmv/4_define.smv Normal file
View File

@ -0,0 +1,18 @@
MODULE main
VAR
x: boolean;
r: boolean;
-- The DEFINE block doesn't really matter?
DEFINE
y := !(x xor r);
ASSIGN
init(r) := FALSE;
next(r) := x xor r;
-- NuSMV -int five.smv
-- go
-- State of system depends only on the variables in the VAR block

View File

@ -0,0 +1,33 @@
MODULE main
VAR
in1: boolean;
in2: boolean;
DEFINE
-- no delay
out := !(in1 & in2);
-- no ASSIGN block => all possible transitions
-- NuSMV > print_reachable_states -v
-- ######################################################################
-- system diameter: 1
-- reachable states: 4 (2^2) out of 4 (2^2)
-- ------- State 1 ------
-- in1 = TRUE
-- in2 = TRUE
-- ------- State 2 ------
-- in1 = TRUE
-- in2 = FALSE
-- ------- State 3 ------
-- in1 = FALSE
-- in2 = TRUE
-- ------- State 4 ------
-- in1 = FALSE
-- in2 = FALSE
-- -------------------------
-- ######################################################################

View File

@ -0,0 +1,14 @@
MODULE main
VAR
in1: boolean;
in2: boolean;
out: boolean;
-- 8 total states now since there are 3 inputs
ASSIGN
-- a unit delay is there.
init(out) := TRUE;
next(out) := !(in1 & in2);

View File

@ -0,0 +1,16 @@
MODULE main
VAR
main_in1: boolean;
main_in2: boolean;
q: nand2(main_in1, main_in2);
MODULE nand2(nand_in1, nand_in2)
VAR
out: boolean;
ASSIGN
-- a unit delay is here
init(out) := TRUE;
next(out) := !(nand_in1 & nand_in2);

28
nusmv/8_modules.smv Normal file
View File

@ -0,0 +1,28 @@
MODULE main
VAR
main_x1: boolean;
main_x2: boolean;
main_y1: boolean;
main_y2: boolean;
main_q1: cust_nand(main_x1, main_x2);
main_q2: cust_nand(main_y1, main_y2);
DEFINE
-- no delay
main_out := main_q1.nand_out xor main_q2.nand_out;
MODULE cust_nand(nand_in1, nand_in2)
VAR
nand_out: boolean;
ASSIGN
-- unit time delay
init(nand_out) := TRUE;
next(nand_out) := !(nand_in1 & nand_in2);
-- There are 64 states because there are 6 states:
- main_x1
- main_x2
- main_y1
- main_y2
- main_q1.out
- main_q2.out

9
nusmv/one.smv Normal file
View File

@ -0,0 +1,9 @@
MODULE main
VAR
location: {l1,l2};
ASSIGN
init(location) := l1;
next(location) := case
(location = l1) : l2;
(location = l2) : l1;
esac;

45
nusmv/three.smv Normal file
View File

@ -0,0 +1,45 @@
MODULE main
VAR
request: boolean;
status: {ready, busy}; -- an enum
ASSIGN
init(status) := ready;
-- init of request not mentioned => 2 * states
next(status) := case
request: busy;
TRUE: {ready, busy}; -- can go anywhere
esac;
-- NuSMV > check_ltlspec -p "G(request=FALSE)"
-- -- specification G request = FALSE is false
-- -- as demonstrated by the following execution sequence
-- Trace Description: LTL Counterexample
-- Trace Type: Counterexample
-- -> State: 1.1 <-
-- request = TRUE
-- status = ready
-- -- Loop starts here
-- -> State: 1.2 <-
-- request = FALSE
-- status = busy
-- -> State: 1.3 <-
-- NuSMV > check_ltlspec -p "F(request=TRUE)"
-- -- specification F request = TRUE is false
-- -- as demonstrated by the following execution sequence
-- Trace Description: LTL Counterexample
-- Trace Type: Counterexample
-- -- Loop starts here
-- -> State: 1.1 <-
-- request = FALSE
-- status = ready
-- -> State: 1.2 <-
-- Combining G and F
-- NuSMV > check_ltlspec -p "G(request=TRUE -> F(status=busy) )"
-- -- specification G (request = TRUE -> F status = busy) is true

40
nusmv/two.smv Normal file
View File

@ -0,0 +1,40 @@
MODULE main
VAR
location: {l1, l2};
x: 0 .. 100; -- only bounded integers
ASSIGN
init(location) := l1;
init(x) := 0;
next(location) := case
(location = l1) & (x < 10): l2;
(location = l2): l1;
TRUE: location; -- no change (like an else clause)
esac;
next(x) := case
--(location = l1): x;
(location = l2) & (x < 100): x + 1;
TRUE: x;
esac;
-- NuSMV -int
-- read_model -i <in.smv>
-- flatten_hierarchy
-- encode_variables
-- build_model
--
-- pick_state -i
-- simulate -i -k 15
-- print_reachable_states -v
-- NuSMV > check_ltlspec -p "G(x>=0)"
-- -- specification G x >= 0 is true
-- NuSMV > check_ltlspec -p "F(x>=5)"
-- -- specification F x >= 5 is true

View File

@ -0,0 +1,91 @@
/*
Ripple carry adder.
Carry out of previous fulladder is given as carry in of next fulladder
*/
// Behavioural
module adder(S, Cy, A, B, C);
input A, B, C;
output S, Cy;
assign S = A ^ B ^ C;
assign Cy = (A & B) | (B & C) | (A & C);
endmodule
/* Structural definition. */
// netlist.
// Can be specified at different levels
// Each successive level reveals more details
// A 4-bit ripple carry adder
// Consists of 4 full adders
// Each full adder has circuits for sum and carry.
module sum (sum, a, b, cy_in);
input a, b, cy_in;
output sum;
wire t;
xor x1 (t, a, b)
xor x2 (sum, cy_in, t)
endmodule
module carry (cy_out, a, b, cy_in);
input a, b, cy_in;
output cy_out;
wire t1, t2, t3;
and g1 (t1, a, b) ;
and g2 (t2, b, c) ;
and g3 (t3, a, c) ;
or g4 (cy_out, t1, t2, t3);
endmodule
module add (cy_out, sum, a, b, cy_in);
input a, b, cy_in;
output sum, cy_out;
sum s1 (sum, a, b, cy_in);
carry c1 (cy_out, a, b, cy_in);
endmodule
primitive add4 (s, cy4, cy_in, x, y);
input [3:0] x, y; // a vector. A 4-bit number here.
input cy_in;
output s, cy4;
// Instantiating the constituent full adders
add
/*
primitive sum(S, A, B, C);
input A, B, C;
output S;
table
0 0 0 : 0;
0 0 1 : 1;
0 1 0 : 1;
0 1 1 : 0;
1 0 0 : 1;
1 0 1 : 0;
1 1 0 : 0;
1 1 1 : 1;
endtable
endprimitive
primitive carry(Cy, A, B, C);
input A, B, C;
output Cy;
table
1 1 ? : 1;
1 ? 1 : 1;
? 1 1 : 1;
0 0 ? : 0;
? 0 0 : 0;
0 ? 0 : 0;
endtable
endprimitive
*/

View File

@ -0,0 +1,27 @@
module testbench;
// Instantiating the 'args' of the module being tested
reg A, B, C, D, E, F; // LHS vars
wire Y; // RHS vars
example DUT(A, B, C, D, E, F, Y);
// initial block will be executed only once
initial
begin
// Following two lines for gtkwave
$dumpfile ("example.vcd"); // vcd: Value Change Dump
$dumpvars (0, testbench); // 0 means all the variables in the
// testbench module
// Monitor these variables. When any of them changes, 'print'.
// $time: simulation time
// %b: bit
$monitor ($time, "A=%b, B=%b, C=%b, D=%b, E=%b, F=%b, Y=%b",
A, B, C, D, E, F, Y);
#5 A=1; B=0; C=0; D=1; E=0; F=0; // wait time 5 units and apply these
// values
#5 A=0; B=0; C=1; D=1; E=0; F=0;
#5 A=1; C=0;
#5 F=1;
#5 $finish;
end
endmodule

View File

@ -0,0 +1,21 @@
/*
As described in https://nptel.ac.in/courses/106/105/106105165/
*/
// A structural netlist
module example (A, B, C, D, E, F, Y);
input A, B, C, D, E, F;
output Y;
wire t1, t2, t3, Y; // Y here is not mandatory
// # denotes delay in seconds
nand #1 G1 (t1, A, B);
and #2 G2 (t2, C, ~B, D); // ~ means NOT
nor #1 G3 (t3, E, F);
nand #1 G4 (Y, t1, t2, t3);
// We used two NAND gates above. We could merge the two statements like:
// nand #1 G1 (t1, A, B), // comma here
// G4 (Y, t1, t2, t3);
endmodule

View File

@ -0,0 +1,5 @@
module simpleand (f, x, y);
input x, y;
output f;
assign f = x & y;
endmodule

View File

@ -0,0 +1,23 @@
module testbench;
reg f, x, y;
simpleand DUT(f, x, y);
initial
begin
$dumpfile ("simpleand.vcd");
$dumpvars (0, testbench);
$monitor ($time, "f=%b, x=%b, y=%b", f, x, y);
#1 x=0; y=0;
#3 x=0; y=1;
#3 x=1; y=0;
#3 x=1; y=1;
#3 $finish;
end
endmodule
/*
-------\
x -->-| |
| |-----> f
y -->-| |
-------/
*/

View File

@ -0,0 +1,42 @@
module testbench;
reg a, b, c, d, e, f;
endmodule
module two_level(a, b, c, d, e, f);
input a, b, c, d, e;
output f;
wire t1, t2; // nets
assign t1 = a & b;
assign t2 = ~(c | d);
assign f = ~(t1 & t2);
endmodule
/* Two level design
|----\
a ---| |
| AND |--- t1 ---|----\
b ---| | | |
|----/ | |
|NAND |--- f
|----\ | |
c ---| | | |
| NOR |--- t2 ---| |
| | |----/
d ---|----/
*/
/*
|----\
a ------------------| |
| & |--- t1 ---|----\
b ------------------| | | |
|----/ | | |---|
| & |--- (t1 & t2) ---| ~ |--- ~(t1 & t2)
|---| |----\ | | |---|
c ---| ~ |--- ~c ---| | | |
|---| | | |--- t2 ---| |
| | |----/
d ------------------|----/
*/

View File

@ -0,0 +1,40 @@
// Behavioural
module carry(S, Cy, A, B, C);
input A, B, C;
output S, Cy;
assign S = A ^ B ^ C;
assign Cy = (A & B) | (B & C) | (A & C);
endmodule
/*
primitive sum(S, A, B, C);
input A, B, C;
output S;
table
0 0 0 : 0;
0 0 1 : 1;
0 1 0 : 1;
0 1 1 : 0;
1 0 0 : 1;
1 0 1 : 0;
1 1 0 : 0;
1 1 1 : 1;
endtable
endprimitive
primitive carry(Cy, A, B, C);
input A, B, C;
output Cy;
table
1 1 ? : 1;
1 ? 1 : 1;
? 1 1 : 1;
0 0 ? : 0;
? 0 0 : 0;
0 ? 0 : 0;
endtable
endprimitive
*/

18
verilog/adder_physical.v Normal file
View File

@ -0,0 +1,18 @@
// A partial version of the physical description of a 4 bit adder
// polysilicon: a high-purity form of silicon. Used in solar cells as well.
// Basically the components are some polygons (mostly rectangles??)
module add4;
input x[3:0], y[3:0], cy_in;
output s[3:0], cy4;
boundary [0, 0, 130, 500]; // coordinates
port x[0] aluminium width=1 origin=[0, 35];
port y[0] aluminium width=1 origin=[0, 85];
port cy_in polysilicon width=2 origin=[70, 0];
port s[0] aluminium width=1 origin=[120, 65];
add a0 origin = [0, 0];
add a1 origin = [0, 120];
endmodule

View File

@ -0,0 +1,45 @@
// Structural definition.
// netlist.
// Can be specified at different levels
// Each successive level reveals more details
// A 4-bit ripple carry adder
// Consists of 4 full adders
// Each full adder has circuits for sum and carry.
module sum (sum, a, b, cy_in);
input a, b, cy_in;
output sum;
wire t;
xor x1 (t, a, b)
xor x2 (sum, cy_in, t)
endmodule
module carry (cy_out, a, b, cy_in);
input a, b, cy_in;
output cy_out;
wire t1, t2, t3;
and g1 (t1, a, b) ;
and g2 (t2, b, c) ;
and g3 (t3, a, c) ;
or g4 (cy_out, t1, t2, t3);
endmodule
module add (cy_out, sum, a, b, cy_in);
input a, b, cy_in;
output sum, cy_out;
sum s1 (sum, a, b, cy_in);
carry c1 (cy_out, a, b, cy_in);
endmodule
primitive add4 (s, cy4, cy_in, x, y);
input [3:0] x, y; // a vector. A 4-bit number here.
input cy_in;
output s, cy4;
// Instantiating the constituent full adders
add